Termination w.r.t. Q proof of /tmp/tmpkFQ69G/toList.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

LISTIFY(n, xs) → APPEND(xs, n)
APPEND(cons(y, ys), x) → APPEND(ys, x)
LISTIFY(n, xs) → RIGHT(n)
LISTIFY(n, xs) → ELEM(left(n))
LISTIFY(n, xs) → RIGHT(left(n))
LISTIFY(n, xs) → ISEMPTY(n)
LISTIFY(n, xs) → ELEM(n)
TOLIST(n) → LISTIFY(n, nil)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
LISTIFY(n, xs) → ISEMPTY(left(n))
LISTIFY(n, xs) → LEFT(n)
LISTIFY(n, xs) → LEFT(left(n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(n, xs) → APPEND(xs, n)
APPEND(cons(y, ys), x) → APPEND(ys, x)
LISTIFY(n, xs) → RIGHT(n)
LISTIFY(n, xs) → ELEM(left(n))
LISTIFY(n, xs) → RIGHT(left(n))
LISTIFY(n, xs) → ISEMPTY(n)
LISTIFY(n, xs) → ELEM(n)
TOLIST(n) → LISTIFY(n, nil)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
LISTIFY(n, xs) → ISEMPTY(left(n))
LISTIFY(n, xs) → LEFT(n)
LISTIFY(n, xs) → LEFT(left(n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 10 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(y, ys), x) → APPEND(ys, x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(y, ys), x) → APPEND(ys, x)

R is empty.
The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(y, ys), x) → APPEND(ys, x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPEND(cons(y, ys), x) → APPEND(ys, x)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) at position [0] we obtained the following new rules:

LISTIFY(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), elem(left(empty)), node(right(left(empty)), elem(empty), right(empty))), y1, append(y1, empty))
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), elem(left(empty)), node(right(left(empty)), elem(empty), right(empty))), y1, append(y1, empty))
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [1,0] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [2] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,0,0] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,1,0] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,2,0,0] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,2,1] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,2,2] we obtained the following new rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, x2)), y1, append(y1, node(x0, x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, x2)), y1, append(y1, node(x0, x1, x2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, x2)), y1, append(y1, node(x0, x1, x2))) at position [1] we obtained the following new rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

left(empty) → empty
right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isEmpty(empty)
isEmpty(node(x0, x1, x2))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

left(empty) → empty
right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2))) at position [3,0] we obtained the following new rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

left(empty) → empty
right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) at position [3,0] we obtained the following new rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

left(empty)
left(node(x0, x1, x2))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) at position [3,1] we obtained the following new rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2))) at position [3,2,0] we obtained the following new rules:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) at position [3,2,0] we obtained the following new rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

right(empty)
right(node(x0, x1, x2))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF(false, false, n, m, xs, ys) → LISTIFY(m, xs) we obtained the following new rules:

IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF(false, true, n, m, xs, ys) → LISTIFY(n, ys) we obtained the following new rules:

IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5) we obtained the following new rules:

IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) we obtained the following new rules:

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0) we obtained the following new rules:

IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2))) we obtained the following new rules:

LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ ForwardInstantiation

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)

The remaining pairs can at least be oriented weakly.

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)

Used ordering: Polynomial interpretation [25]:

POL(IF(x₁, x₂, x₃, x₄, x₅, x₆)) = x₂ + x₄
POL(LISTIFY(x₁, x₂)) = 1 + x₁
POL(append(x₁, x₂)) = x₁
POL(cons(x₁, x₂)) = 0
POL(elem(x₁)) = 0
POL(empty) = 1
POL(false) = 1
POL(nil) = 1
POL(node(x₁, x₂, x₃)) = x₁ + x₃
POL(true) = 0
POL(y) = 0

The following usable rules [17] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ ForwardInstantiation

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ QDPOrderProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ ForwardInstantiation

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ QDPOrderProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

elem(node(x0, x1, x2))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ ForwardInstantiation

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ QDPOrderProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ QReductionProof

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))

The remaining pairs can at least be oriented weakly.

IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

Used ordering: Polynomial interpretation with max and min functions [25]:

POL(IF(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄
POL(LISTIFY(x₁, x₂)) = x₁
POL(append(x₁, x₂)) = 0
POL(cons(x₁, x₂)) = 0
POL(false) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = 1 + x₁ + x₂
POL(y) = 0

The following usable rules [17] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ QReductionProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ UsableRulesProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ QReductionProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Instantiation

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ ForwardInstantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ ForwardInstantiation

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ ForwardInstantiation

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ ForwardInstantiation

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ QDPOrderProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ QReductionProof

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ QDPOrderProof

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

append(nil, x0)
append(cons(y, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.